1. Technical Field
The present invention generally relates to reachability analysis for hybrid systems and, more particularly, to systems and methods for determining reachable states of a hybrid system by employing template polyhedra.
2. Description of the Related Art
In general, hybrid systems verification, even for simple systems, have presented a complex and difficult challenge. Too coarse an approximation may not enable proving the property of interest while analytic solutions are hard to obtain. Numerous approaches have been employed in the past to solve reachability queries, of which a few related approaches are mentioned below.
One such approach includes using polyhedra to determine reachable states of rectangular hybrid systems, as applied by the “HyTech” tool. More complex dynamics have been handled by abstraction. Other approaches deal with systems having complex dynamics by symbolically integrating them. For example, computing flowpipe segments by optimizing the bounding functions using a non-convex optimization problem has been employed in some known polyhedral flowpipe approximation approaches. In addition, approaches have included constructing ellipsoidal approximations; using level-set methods; using orthogonal polyhedra and face lifting; and generating approximations to a flowpipe based on quantifier elimination over the reals along with Taylor series expansions.
Additionally, other techniques for proving safety of a hybrid system by symbolically integrating its dynamics have been presented. Recently, symbolic techniques for generating reachable regions without the use of an explicit flowpipe approximation have been proposed, including the generation of polynomial equality invariants for systems with polynomial dynamics. These techniques can handle nonlinear systems beyond the reach of many related techniques, but the theory has so far been restricted to equality invariants. Further, a method for the synthesis of barrier functions (inequalities) has been proposed to justify invariants of nonlinear systems using convex optimization. These barrier functions are generated by solving equations on the unknown coefficients of a parametric polynomial.
The reachability problem for autonomous linear systems has also been solved by resorting to a series of geometric programs. Further, zonotopes have been used to construct flowpipes for uncertain linear systems. A different approach solves the reachability problem for hybrid systems by repeatedly subdividing the invariant region and approximating the dynamics inside each subdivision by piece-wise constant dynamics.
Turning now to known uses of policy iteration and invariants, the concept of a relaxed invariant used in a policy iteration scheme first appeared in SANKARANARAYANAN, S., SIPMA, H. B., AND MANNA, Z., Fixed point iteration for computing the time-elapse operator, in Hybrid Systems: Computation and Control (HSCC 2006), to appear (2006), Lecture Notes in Computer Science, Springer-Verlag. The invariant was computed using polyhedra as the fixed point of a refinement operator over cones of functions. A widening heuristic was used to force convergence.
In addition, invariants have been computed in static analysis of programs by using template polyhedra. For example, boxes have been used to represent sets of states in the interval domain. Similarly, template polyhedron of the form ±xi±xj≦c have been used in the octagon domain. General template polyhedra have also been used to represent sets of states. Recently, techniques such as policy iteration and strategy iteration have been employed to compute the least fixed point for the interval, octagon and the template polyhedra domain.
Template polyhedra have also appeared implicitly in the work of Chutinan and Krogh, which is a part of the Checkmate tool. SILVA, B., RICHESON, K., KROGH, B. H., AND CHUTINAN, A. Modeling and verification of hybrid dynamical system using checkmate, in ADPM 2000 (2000). Their approach chooses a series of bounding half-spaces (affine functions) g1, . . . , gm to compute a given flowpipe segment for a time instance. The resulting flowpipe segment is expressed in terms of a template polyhedron igi≦ci.
It should also be noted, regarding set-valued integration, known techniques apply numerical integration schemes by using analysis over set valued functions and include schemes that are analogous to popular numerical integration schemes such as Runge-Kutta. However, the sets used in these schemes are arbitrary and not, as such, restricted to intersections of bounding half-spaces.
Returning to known hybrid system verification methods discussed above, there has typically been a trade-off between expressiveness and tractability. Polyhedra have been widely used to represent sets of states for the verification of safety as well as liveness properties. However, the complexity of the basic algorithms involving polyhedra such as convex hull, post condition across discrete transitions and flowpipe construction is worst-case exponential. In practice, this fact has limited the usefulness of verification tools for hybrid systems. Therefore, approaches to verifying systems have been based on restricted forms of polyhedra such as orthogonal polyhedra and zonotopes. Likewise, predicate abstraction, a popular technique for verifying systems, uses boolean combinations of a given set of predicates p1, . . . pm, to represent sets of states.
Furthermore, existing solutions to hybrid systems verification are limited by two aspects: (a) the number of discrete modes in the system and (b) the number of continuous variables. The number of continuous variables and the complexity of continuous dynamics in hybrid systems is a principal challenge in the verification and analysis of such systems. Although existing techniques seem to yield sufficient results for continuous systems, such as techniques employing zonotopes, for example, discussed above, they are difficult to apply to systems in which the number of modes is large.
Accordingly, there is a need for a more efficient means of determining over-approximations of reachable states of hybrid systems. In addition, there is also a need for an approach to determining over-approximations of reachable states of hybrid systems that may be applied to large systems with a substantial number of modes and continuous variables.